'''
Created on 2011-09-07

@author: kacper
'''
import unittest
from dataStructs.formulaSet import Theory
from parsing.parser import sents_parse_string
from dataStructs.definitions import Const, Var

class Test(unittest.TestCase):


    def setUp(self):
        self.aVar = sents_parse_string('A')[0]
        self.aConst = sents_parse_string('a')[0]

    def tearDown(self):
        pass


    def testSimpleSubst(self):
        th = Theory()
        fo1 = sents_parse_string("A || B || A || C")[0]
        fo1 = fo1.substitute(self.aVar, self.aConst)
        print fo1 
        self.assertFalse( Var('A') in fo1.getVariables())
        self.assertTrue("a" in fo1.prt())


    def testRelSubstitute(self):
        th = Theory()
        fo1 = sents_parse_string("r(A,A,B)")[0]
        fo1 = fo1.substitute(self.aVar, self.aConst)
        print fo1 
        self.assertFalse( Var('A') in fo1.getVariables())
        self.assertTrue("a" in fo1.prt())
        
    def testTypes(self):
        th = Theory()
        fo1 = sents_parse_string("r(A,A,b)")[0]
        fo1 = fo1.substitute(self.aVar, self.aConst)
        lstTypes =filter( lambda x:x.__class__ != Const, fo1.args) 
        self.assertTrue(lstTypes ==[] )
        
        


if __name__ == "__main__":
    #import sys;sys.argv = ['', 'Test.testSimpleSubst']
    unittest.main()